Skip to content

Add various categories with subobject classifiers - #371

Merged
ScriptRaccoon merged 13 commits into
mainfrom
empty-or-finite-pairs-of-sets
Sep 26, 2026
Merged

Add various categories with subobject classifiers#371
ScriptRaccoon merged 13 commits into
mainfrom
empty-or-finite-pairs-of-sets

Conversation

@ScriptRaccoon

@ScriptRaccoon ScriptRaccoon commented Sep 13, 2026 •
edited
Loading

Copy link
Copy Markdown
Owner

This PR adds various examples of categories with subobject classifiers and finite limits*, while not satisfying some other properties. The goal is to reduce the number of missing combinations, cf. this milestone. The categories are listed below. Most of their properties have been decided; only the question if F(I)-Set is cototal remains open for now.

*This is currently included in the definition of a subobject classifier, but might change later (#370).

The category of finite-or-empty pairs of sets

This is a rather random category, the full subcategory of Set × Set consisting of pairs (A,B) where A is empty or B is finite. It serves as an example of a category with a subobject classifier, but without binary coproducts.

All properties have been decided.

The category of directed graphs with finite components

This is the full subcategory of DiGraph consisting of coproducts of finite directed graphs. It is an example of a category with a subobject classifier, but without coequalizers.

All properties have been decided.

The category of sequences of sets

This is the functor category [(N,≤),Set]. It shares exactly the same recorded properties (currently) as the Sierpinski topos Mor(Set). (But they are not equivalent, since for example the Sierpinski topos has finitely many subterminals, but the category of sequences has infinitely many.) In particular, all properties have been decided, and no new combinations are witnessed. I have added this category to prepare for the next example.

The category of connected sequences of sets

We also add the full subcategory of [(N,≤),Set] consisting of connected sequences $X_0 \to X_1 \to \cdots$, meaning that $colim_n X_n$ is a singleton. It has been suggested by Jonas Frey at mathoverflow and provides an example of a category with a subobject classifier, but without initial object (and no binary copowers, hence also no binary coproducts, just like the first category in the list).

All properties have been decided (this was a lot of work).

The category of Z-sets

This category is an instance of the category of M-sets, but the difference is that the property of being semi-strongly connected can be decided (it is not). It turns out that it has exactly the same properties as the Jónsson-Tarski topos (w.r.t. the recorded properties). Thus, all properties have been decided, no new combinations are witnessed, but this category prepares for the next example.

The category of finite Z-sets

This category is an example of a category with a subobject classifier, in fact even an elementary topos, without a cogenerator (and also without a generator, but for this we already knew several examples).

All properties have been decided.

The category of F(I)-sets

Here, F(I) is a large free group. The category of F(I)-sets provides an example of a category with a subobject classifier, in fact a complete and cocomplete elementary topos, that does not have a cogenerating collection.

All properties except for one have been designed: if it is cototal. This appears to be a very difficult problem.

New combinations

In total, the categories satisfy 72 new combinations. The number of missing combinations goes down from 393 to 321.

pnpm db:combinations category SetxSet_0_fin DiGraph_fc SeqSet_conn Z-FinSet 'F(I)-Set'

Found 72 unique witnessed combinations by the supplied structures (SetxSet_0_fin, DiGraph_fc, SeqSet_conn, Z-FinSet, F(I)-Set):

Directly witnessed:
- subobject classifier ∧ ¬Barr-coexact
- subobject classifier ∧ ¬Barr-exact
- subobject classifier ∧ ¬co-Malcev
- regular subobject classifier ∧ ¬coequalizers
- subobject classifier ∧ ¬coequalizers
- subobject classifier ∧ ¬coregular
- subobject classifier ∧ ¬effective congruences
- subobject classifier ∧ ¬finitely cocomplete
- subobject classifier ∧ ¬pushouts
- regular subobject classifier ∧ ¬quotients of congruences
- subobject classifier ∧ ¬quotients of congruences
- ℵ₁-accessible ∧ ¬quotients of congruences
- ℵ₁-filtered colimits ∧ ¬quotients of congruences
- regular subobject classifier ∧ ¬reflexive coequalizers
- subobject classifier ∧ ¬reflexive coequalizers
- subobject classifier ∧ ¬regular
- elementary topos ∧ ¬cogenerating collection
- pretopos ∧ ¬cogenerating collection
- quasitopos ∧ ¬cogenerating collection
- regular subobject classifier ∧ ¬cogenerating collection
- subobject classifier ∧ ¬cogenerating collection
- elementary topos ∧ ¬cogenerator
- pretopos ∧ ¬cogenerator
- quasitopos ∧ ¬cogenerator
- regular subobject classifier ∧ ¬cogenerator
- subobject classifier ∧ ¬cogenerator
- elementary topos ∧ ¬extremal cogenerating collection
- pretopos ∧ ¬extremal cogenerating collection
- quasitopos ∧ ¬extremal cogenerating collection
- subobject classifier ∧ ¬extremal cogenerating collection
- elementary topos ∧ ¬extremal cogenerator
- pretopos ∧ ¬extremal cogenerator
- subobject classifier ∧ ¬extremal cogenerator
- subobject classifier ∧ ¬binary copowers
- subobject classifier ∧ ¬binary coproducts
- subobject classifier ∧ ¬disjoint finite coproducts
- subobject classifier ∧ ¬finite copowers
- subobject classifier ∧ ¬finite coproducts
- subobject classifier ∧ ¬initial object
- subobject classifier ∧ ¬multi-initial object
- subobject classifier ∧ ¬ℵ₁-cofiltered
- exact filtered colimits ∧ ¬ℵ₁-cofiltered limits

Dually witnessed:
- quotient object classifier ∧ ¬Barr-exact
- quotient object classifier ∧ ¬Barr-coexact
- quotient object classifier ∧ ¬Malcev
- regular quotient object classifier ∧ ¬equalizers
- quotient object classifier ∧ ¬equalizers
- quotient object classifier ∧ ¬regular
- quotient object classifier ∧ ¬effective cocongruences
- quotient object classifier ∧ ¬finitely complete
- quotient object classifier ∧ ¬pullbacks
- regular quotient object classifier ∧ ¬coquotients of cocongruences
- quotient object classifier ∧ ¬coquotients of cocongruences
- ℵ₁-cofiltered limits ∧ ¬coquotients of cocongruences
- regular quotient object classifier ∧ ¬coreflexive equalizers
- quotient object classifier ∧ ¬coreflexive equalizers
- quotient object classifier ∧ ¬coregular
- regular quotient object classifier ∧ ¬generating collection
- quotient object classifier ∧ ¬generating collection
- regular quotient object classifier ∧ ¬generator
- quotient object classifier ∧ ¬generator
- quotient object classifier ∧ ¬extremal generating collection
- quotient object classifier ∧ ¬extremal generator
- quotient object classifier ∧ ¬binary powers
- quotient object classifier ∧ ¬binary products
- quotient object classifier ∧ ¬disjoint finite products
- quotient object classifier ∧ ¬finite powers
- quotient object classifier ∧ ¬finite products
- quotient object classifier ∧ ¬terminal object
- quotient object classifier ∧ ¬multi-terminal object
- quotient object classifier ∧ ¬ℵ₁-filtered
- exact cofiltered limits ∧ ¬ℵ₁-filtered colimits

@ScriptRaccoon ScriptRaccoon added the data additions and updates to the database label Sep 13, 2026
@ScriptRaccoon
ScriptRaccoon force-pushed the empty-or-finite-pairs-of-sets branch from 31c216c to 19a72ed Compare September 14, 2026 20:17
@ScriptRaccoon ScriptRaccoon changed the title Add the category of empty-or-finite pairs of sets Add various categories with subobject classifiers Sep 14, 2026
@ScriptRaccoon
ScriptRaccoon force-pushed the empty-or-finite-pairs-of-sets branch 7 times, most recently from 8ecf9a2 to b8d4fd3 Compare September 21, 2026 09:25
@ScriptRaccoon
ScriptRaccoon force-pushed the empty-or-finite-pairs-of-sets branch from ae8ee9a to c240d3f Compare September 24, 2026 06:10
@ScriptRaccoon
ScriptRaccoon force-pushed the empty-or-finite-pairs-of-sets branch from c240d3f to 067b0bd Compare September 24, 2026 06:34
@ScriptRaccoon
ScriptRaccoon force-pushed the empty-or-finite-pairs-of-sets branch from 1ad571a to 16aec30 Compare September 25, 2026 17:58
@ScriptRaccoon
ScriptRaccoon merged commit 28dc979 into main Sep 26, 2026
1 check passed
@ScriptRaccoon
ScriptRaccoon deleted the empty-or-finite-pairs-of-sets branch September 26, 2026 19:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

data additions and updates to the database

Projects

None yet

Milestone

Add categories that witness new prope...

Development

Successfully merging this pull request may close these issues.

1 participant

@ScriptRaccoon